Issue2079.agda:34,6-11
The case for the constructor nec is impossible
because unification ended with a conflicting equation
  ∅ ≟ Γ , A
Possible solution: remove the clause, or use an absurd pattern ().
when checking that the pattern nec t has type (Γ , A) ⊢ B
